| Definitions | p-outcome(p), fpf-ap(f; eq; x), Kind-deq, locl(a), decl-state(ds), fpf-dom(eq; x; f),  x.A(x),  x. t(x), ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), ecl-machine1{$ecl:ut2}(i; ds; da; A), R-state-var-init(i; ds; da; x; T; v; ks; tr), R-state-var(i; ds; da; x; T; ks; tr), Rinit(loc; T; x; v), Rframe(loc; T; x; L), Rall(L; x.R(x)), Reffect(loc; ds; knd; T; x; f), inl x , ma-valtype(da; k), fpf-join(eq; f; g), id-deq, fpf-single(x; v), mkid{$x:ut2}, Knd, es realizer ind Rinit compseq tag def, es realizer ind Rframe compseq tag def, ecl-trans(x), ecl-trans-tuple{i:l}(ds; da), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), Rpre(loc; ds; a; p; P), Rplus(left; right), ecl-machine3(ds; da; x; T; ks; a; snd), ecl-machine2(i; ds; da; x; T; ks; a; upd), R-has-loc(R; i), es realizer ind Rplus compseq tag def, es realizer ind Rpre compseq tag def, left + right, Unit, P    Q,   b, eq_id(a; b),  , sqequal(s; t), prop{i:l}, sq_type(T), guard(T), True, P Q,  x:A. B(x), top, isect(A; x.B(x)), t  T, void, type List, Type, R-compat{i:l}(A; B), f(a), if b then t else f fi , fpf-compatible(A; a.B(a); eq; f; g), x:A  B(x), finite-prob-space, {x:A| B(x)} , R-Feasible{i:l}(R), es realizer ind, A, False, msg-spec-loc-decl(snd; i; da), s = t, l_all(L; T; x.P(x)), update-spec-decl(upd; ds),  b, update-spec(ds; da), msg-spec(ds; da), ecl(ds; da), rec(x.A(x)), fpf(A; a.B(a)), x:A  B(x), Id, atom{$n:n}, P  Q, A c B, rationals, decl-type{i:l}(ds; x), fpf-sub(A; a.B(a); eq; f; g), x(s), P Q, EqDecider(T),  T, es realizer ind Reffect compseq tag def, a < b, (x l),  x:A. B(x), case b of inl(x) => s(x) | inr(y) => t(y), inr x , R-loc(R), Rds(R), Rda(R), R-base-domain(R), eq_bd(p; q), R-frame-compat(A; B), R-interface-compat(A; B), Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), Rframe?(x1), Rframe-x(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Reffect-ds(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsframe-tag(x1), Rsends-g(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rrframe?(x1), Rrframe-x(x1), Rpre-ds(x1), Rpre-a(x1), Rrframe-L(x1), Reffect-knd(x1), Reffect-T(x1), Rsends?(x1), Rsends-knd(x1), Rsends-l(x1), Rsends-dt(x1), Rsends-T(x1), (i = j), R-discrete_compat(A; B), Reffect-discrete(A), Rinit-discrete(A), Reffect?(x1), Reffect-x(x1), Reffect-f(x1), Rinit?(x1), Rinit-x(x1), Rinit-v(x1), <a, b>, fpf-cap(f; eq; x; z), update-spec-vars(upd), l[i],  , A  B, ||as||, #$n, P  Q, IdLnk, list_accum(x,a.f(x;a); y; l), [], x,y. t(x;y), qeq(r; s), tt, equiv_rel(T; x,y.E(x;y)), b-union(A; B), int_nzero,  , let x,y = A in B(x;y), quotient(A; x,y.B(x;y)), t.1, product-deq(A; B; a; b), t.2, ma-state(ds), remove-repeats(eq; L), idlnk-deq, msg-spec-links(snd), R-lnk-tags(ds; da; l; tgs; ks; g), suptype(S; T), subtype(S; T), rcv(l,tg), lnk-decl(l; dt), isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), Rsends(ds; knd; T; l; dt; g), ecl-m3(a; snd; x; l), es-dt(l; da), es realizer ind Rsends compseq tag def, ecl-tags(l; snd), source(l), Rsframe(lnk; tag; L), es realizer ind Rsframe compseq tag def |
| Lemmas | lsrc wf, Rsframe wf, false wf, lnk-decl-compatible-single, es-dt wf, lnk-decl wf, rcv wf, es-dt-cap, fpf-cap-void-subtype, Rsends wf, ecl-m3 wf, ecl-tags wf, R-lnk-tags wf, msg-spec-links wf, idlnk-deq wf, remove-repeats wf, decl-state-subtype, fpf-single-dom, or functionality wrt iff, fpf-cap-join-subtype, ifthenelse wf, list accum wf, product-deq wf, pi2 wf, pi1 wf, l member wf, fpf-compatible-single-iff, ma-valtype wf, fpf-join wf, decl-type wf, btrue wf, qeq wf2, int nzero wf, b-union wf, quotient wf, rationals wf, IdLnk wf, fpf-join-dom2, R-state-var-compat-unequal-loc, true wf, squash wf, fpf-compatible-single, select wf, length wf1, nat wf, R-state-var wf, update-spec-vars wf, top wf, Knd sq, fpf-empty-compatible-left, fpf-compatible-single2, fpf-compatible-symmetry, assert-eq-knd, fpf-compatible-singles, fpf-compatible-join2, Rpre wf, subtype rel self, eqof eq btrue, fpf-cap-single, fpf-join-cap-sq, fpf-sub weakening, fpf-single wf, fpf-sub-join-left2, subtype-fpf-cap-top, fpf-cap wf, subtype rel dep function, Reffect wf, R-compat-Rall2, R-compat-Rplus-sq, R-compat-symmetry, Id sq, bool wf, eq id wf, assert wf, not wf, bnot wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, R-compat-disjoint, ecl-trans-tuple wf, ecl-trans wf, ecl-machine-loc, ecl-disjoint-compatible, Id wf, fpf wf, Knd wf, ecl wf, msg-spec wf, update-spec wf, update-spec-decl wf, msg-spec-loc-decl wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, ecl-machine wf, R-Feasible wf, finite-prob-space wf, decl-state wf, fpf-compatible wf, locl wf, Kind-deq wf, fpf-ap wf, p-outcome wf |
upd:update-spec(ds; da).